\documentclass[xcolor=table]{beamer}

\usepackage{lmodern}

\usepackage[utf8]{inputenc}
\usepackage{xcolor}
\usepackage{epic, eepic, pgf, tikz}
\usepackage{fancyvrb}
\usepackage{verbatim}

\usetikzlibrary{shapes,arrows,shadows,automata,external,patterns}
\usetikzlibrary{positioning}

%\usetheme{boadilla}
\usecolortheme{seagull}

% Begin definitions
% ------------------------------------------------------------------------------------------------------------------
\setbeamersize{text margin left=1em,text margin right=1em}
\setbeamerfont{title}{size=\LARGE}
\setbeamerfont{author}{size=\large}
\pgfdeclareimage[width=12.8 cm]{layout_image}{first_slide_figure}
\pgfdeclareimage[width=13.2 cm]{top_image}{top}

\setbeamertemplate{title page}{
\vskip0.72cm
% Title and subtitle
\begin{beamercolorbox}[center]{title}
  \usebeamerfont{title}\inserttitle\par%
  \ifx\insertsubtitle\@empty%
  \else%
    \vskip0.25em%
    {\usebeamerfont*{subtitle}\usebeamercolor*[fg]{subtitle}\insertsubtitle\par}%
  \fi%
\end{beamercolorbox}%

\vskip1em\par

% Display author(s)
\begin{beamercolorbox}[center]{author}
  \usebeamerfont{author}\insertauthor{}
\end{beamercolorbox}

\vskip0em\par

% Institute
\begin{beamercolorbox}[center]{institute}
  \usebeamerfont{institute}\insertinstitute{}
\end{beamercolorbox}

\vskip0.4em\par

\begin{beamercolorbox}[center]{institute}
\small Joint work with: P. A. Crocker, M. J. Frade, A. P. Martins, and S. Melo de Sousa
\end{beamercolorbox}

\vskip0.5em%

% Date
\begin{beamercolorbox}[center]{date}
  \usebeamerfont{date}\insertdate
\end{beamercolorbox}

\vskip0.28em


\pgfdeclareverticalshading{beamer@aboveframetitle}{\the\paperwidth}{
         color(0ex)=(myblue!20);
         color(0.5ex)=(myblue!70);
         color(0.5ex)=(white)
}


\begin{beamercolorbox}[wd=1\paperwidth,ht=0.3ex]{author in head/foot}
\pgfuseshading{beamer@aboveframetitle}
\end{beamercolorbox}

\nointerlineskip

\setbeamercolor*{author in head/foot}{bg=myblue!20}
\begin{beamercolorbox}[wd=1\paperwidth,ht=4.15cm,center]{author in head/foot}
\pgfuseimage{layout_image}
\end{beamercolorbox}
%}
%\vskip-5cm

%\vskip-0.6cm
%\pgfuseimage{layout_image}
}

\definecolor{myblue}{RGB}{128,162,210}
\setbeamercolor*{author in head/foot}{bg=myblue!50}
\setbeamercolor*{title in head/foot}{bg=myblue!30}
\setbeamercolor*{date in head/foot}{bg=myblue!15}
\setbeamertemplate{footline}{
  \leavevmode%
  \hbox{%
  \begin{beamercolorbox}[wd=.333333\paperwidth,ht=2.25ex,dp=1ex,center]{author in head/foot}%
    \usebeamerfont{author in head/foot}\insertsectionhead
  \end{beamercolorbox}%
  \begin{beamercolorbox}[wd=.333333\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}%
    \usebeamerfont{title in head/foot}\insertsubsectionhead
  \end{beamercolorbox}%
  \begin{beamercolorbox}[wd=.333333\paperwidth,ht=2.25ex,dp=1ex,right]{date in head/foot}%
    \centering \insertframenumber{} / \inserttotalframenumber
  \end{beamercolorbox}}%
  \vskip0pt%
}


\usebeamerfont*{headline}
    \colorlet{global.bg}{bg}
    \usebeamercolor{subsection in head/foot}
    \usebeamercolor{section in head/foot}
    \usebeamercolor{frametitle}

     \pgfdeclareverticalshading{beamer@belowframetitle}{\the\paperwidth}{%
      color(0ex)=(global.bg);%
      color(1ex)=(frametitle.bg)
    }

\setbeamertemplate{frametitle}
{%
\nointerlineskip%
  \usebeamerfont{headline}%
  \begin{beamercolorbox}[wd=\paperwidth,ht=0.62cm]{empty}
    \pgfuseimage{top_image}
  \end{beamercolorbox}
  \nointerlineskip
\ifx\insertframesubtitle\empty
\vskip0.05cm
  \begin{beamercolorbox}[wd=\paperwidth,ht=.5ex,dp=0ex]{empty}
    \pgfuseshading{beamer@belowframetitle}
  \end{beamercolorbox}
\vskip-0.56cm
\else
\vskip-0.46cm
\fi
  \nointerlineskip%
  \begin{beamercolorbox}[wd=\paperwidth,leftskip=.3cm,rightskip=.3cm plus1fil,vmode]{frametitle}
    \usebeamerfont*{frametitle}\color{myblue!20!black}\insertframetitle%
      \ifx\insertframesubtitle\empty
      \else
        \par{\usebeamerfont*{framesubtitle}{\usebeamercolor[fg]{framesubtitle}\color{black!50!myblue}\insertframesubtitle}\strut\par}%
      \fi%%
    \usebeamerfont{headline}%
  \end{beamercolorbox}%
\ifx\insertframesubtitle\empty
\vskip0.15cm
\else
\vskip0.1mm
\nointerlineskip
  \begin{beamercolorbox}[wd=\paperwidth,ht=.5ex,dp=0ex]{empty}
      \pgfuseshading{beamer@belowframetitle}
  \end{beamercolorbox}%
\vskip-0.1cm
\fi
}


\setbeamertemplate{navigation symbols}{}


\setbeamertemplate{itemize items}[default]
\setbeamertemplate{enumerate items}[default]
\setbeamertemplate{sections/subsections in toc}[square]

%\setbeamercolor{title}{fg=black}
\setbeamercolor{section number projected}{bg=orange,fg=white}
\setbeamercolor{subsection number projected}{bg=green!30!yellow!80!black,fg=white}
\setbeamercolor{frametitle}{fg=blue!40!black}

% ------------------------------------------------------------------------------------------------------------------
% End definitions

\title[T3S-Tool presentation]{T3S Tool - Learning stochastic automata from sample executions}
\author{André de Matos Pedro}
\institute{University of Minho, Braga, Portugal}
%\course{Master in Computer Science}
\date{July 20, 2012}

%\pgfdeclareimage[width=12.2cm,height=3.4cm]{initlogo}{logo}

\begin{document}

%\AtBeginSection[]
%{
%\begin{frame}{Contents}
%\tableofcontents[currentsection]
%\end{frame}
%}

{
\setbeamertemplate{footline}{} 
\begin{frame}
\titlepage
\end{frame}
}
\addtocounter{framenumber}{-1}

\begin{frame}
\frametitle{Contents}
\tableofcontents
\end{frame}


\section{Motivation and Contextualization}

\begin{frame}
\frametitle{Motivation}
\begin{itemize}
\only<1>{\item There are \textbf{learning solutions} for continuous-time Markov processes \textbf{but not for} (the more extensive class) \emph{generalized semi-Markov processes} that is our main goal.
\vskip0.3cm
\item This work is introduced in the following Master thesis and paper:
\begin{itemize}
\item André de Matos Pedro. Learning and testing stochastic discrete event systems. Master's thesis, Universidade do Minho, Portugal, December 2011.
\item André de Matos Pedro, Paul Andrew Crocker and Simão Melo de Sousa. Learning stochastic timed automata from sample executions. To appear in ISoLA12.

\end{itemize}

}

\end{itemize}

\end{frame}

\begin{frame}{Contextualization}

\begin{itemize}
\item \textbf{Learning} a generalized semi-Markov process (GSMP) from \textbf{sample executions} allows to:
\begin{itemize}
\item \textbf{cover a wider range} of stochastic systems than conventional stochastic processes such as \emph{Discrete-Time Markov Chains} (DTMC) and \emph{Continuous-Time Markov Chains} (CTMC),
\item use a GSMP as \textbf{abstraction model} for \emph{stochastic discrete event systems} (SDES),
\item \textbf{verify} the model through \emph{statistical model checking} techniques,
\item provide \textbf{performance evaluations} about systems, and
\item \textbf{achieves} a more general/\textbf{abstract model}.
\end{itemize}
\end{itemize}
\end{frame}


\section{Learning stochastic automata from sample executions}

\begin{frame}
\frametitle{Overview of T3S algorithm}

\begin{center}
\vskip-0.2cm
\begin{tikzpicture}[node distance=8.6cm]
\tikzstyle{every state}=[fill=white,draw=black,text=black]

\node[state,rectangle, rounded corners, fill=myblue!30, inner sep=5pt, scale=0.5] (start) {
\begin{tikzpicture}[->, >=stealth', shorten >=1pt, auto, node distance=1.5cm, semithick]
\node[state] (0) {};
\node[state] (1) [below of=0] {};
\node[state] (2) [below of=1] {};
\node[state] (3) [below of=2] {};
\node[state] (4) [below of=3] {};
\node[state] (5) [below of=4] {};

\node[state] (6) [right of=0] {};
\node[state] (7) [below of=6] {};
\node[state] (8) [below of=7] {};
\node[state] (9) [below of=8] {};
\node[state] (10) [below of=9] {};
\node[state] (11) [below of=10] {};

\node[state] (12) [right of=6] {};
\node[state] (13) [below of=12] {};
\node[state] (14) [below of=13] {};
\node[state] (15) [below of=14] {};
\node[state] (16) [below of=15] {};
\node[state] (17) [below of=16] {};

\node[state] (18) [right of=12] {};
\node[state] (19) [below of=18] {};
\node[state] (20) [below of=19] {};
\node[state] (21) [below of=20] {};
\node[state] (22) [below of=21] {};
\node[state] (23) [below of=22] {};

\path (0) edge [] node {a} (1)
(1) edge [] node {b} (2)
(2) edge [] node {a} (3)
(3) edge [] node {c} (4)
(4) edge [] node {a} (5);

\path (6) edge [] node {b} (7)
(7) edge [] node {a} (8)
(8) edge [] node {b} (9)
(9) edge [] node {c} (10)
(10) edge [] node {d} (11);

\path (12) edge [] node {a} (13)
(13) edge [] node {b} (14)
(14) edge [] node {c} (15)
(15) edge [] node {c} (16)
(16) edge [] node {b} (17);

\path (18) edge [] node {b} (19)
(19) edge [] node {b} (20)
(20) edge [] node {d} (21)
(21) edge [] node {c} (22)
(22) edge [] node {a} (23);
\end{tikzpicture}
};

\node[state,rectangle, rounded corners, fill=myblue!30, scale=0.5] (middle) [right of=start]{
\begin{tikzpicture}[->, >=stealth', shorten >=1pt, auto, node distance=1.8cm, semithick]
\node[state] (0) {};
\node[state] (1) [below left of=0] {};
\node[state] (2) [below right of=0, node distance=3.5cm] {};
\node[state] (3) [below of=1] {};
\node[state] (4) [below left of=2] {};
\node[state] (5) [below right of=2] {};
\node[state] (6) [below left of=3] {};
\node[state] (7) [below right of=3]{};
\node[state] (8) [below of=6]{};
\node[state] (9) [below of=7]{};
\node[state] (10) [below of=8]{};
\node[state] (11) [below of=9]{};
\node[state] (12) [below of=4]{};
\node[state] (13) [below of=5]{};
\node[state] (14) [below of=12]{};
\node[state] (15) [below of=13]{};
\node[state] (16) [below of=14]{};
\node[state] (17) [below of=15]{};

\path (0) edge [above,left] node {a} (1)
(0) edge [below,right] node {b} (2);

\path (1) edge [above,left] node {b} (3);

\path (2) edge [above,left] node {a} (4)
(2) edge [below,right] node {b} (5);

\path (3) edge [above,left] node {a} (6)
(3) edge [below,right] node {c} (7);

\path (6) edge [above,left] node {c} (8);

\path (7) edge [above,left] node {c} (9);

\path (8) edge [above,left] node {a} (10);

\path (9) edge [above,left] node {b} (11);

\path (4) edge [above,right, node distance=1cm] node {b} (12);

\path (5) edge [above,right, node distance=1cm] node {d} (13);

\path (12) edge [above,right, node distance=1cm] node {c} (14);

\path (13) edge [above,right, node distance=1cm] node {c} (15);

\path (14) edge [above,right, node distance=1cm] node {d} (16);

\path (15) edge [above,right, node distance=1cm] node {a} (17);
\end{tikzpicture}
};

\node[state,rectangle, rounded corners, fill=orange!30, scale=0.5] (end) [right of=middle]{
\begin{tikzpicture}[->, >=stealth', shorten >=1pt, auto, node distance=3.5cm, semithick]
\node[state] (0) {};
\node[state] (1) [below left of=0] {};
\node[state] (2) [below of=0] {};
\node[state] (3) [below right of=0] {};

\path (0) edge [above,left] node {a} (1)
(0) edge [left] node {b} (2)
(0) edge [below,right] node {d} (3);

\path (1) edge [] node {b} (2);

\path (2) edge [bend left] node {a} (1);

\path (1) edge [bend left] node {c} (0);

\path (2) edge [bend right,right] node {c} (0);

\path (3) edge [bend left] node {c} (2);

\path (0) edge [bend left] node {c} (3);

\path (3) edge [above] node {b} (2);
\end{tikzpicture}
};

\path (start.east) edge [>=stealth,->, line width=1mm] node {} (middle.west);

\path (middle.east) edge [>=stealth,->, line width=1mm,below] node (tt) {} (end.west);

\node[draw=black, fill=white, text=black, above=5pt,rectangle, rounded corners] at (start.north) {Sample executions};

\node[draw=black, fill=white, text=black, above=5pt,rectangle, rounded corners] at (middle.north) {Event-driven prefix tree};

\node[draw=black, fill=white, text=black, above=5pt,rectangle, rounded corners] at (end.north) {Stochastic automaton};

\node[draw=orange!70!black!90, fill=white, text=orange!70!black!90,rectangle, below=3cm, scale=0.9,rounded corners] (ss) at (tt) {\begin{minipage}{6.8cm}\centering The magic occurs here, based on a \textbf{well defined stable equivalence relation}.\end{minipage}};

\path (ss.north) edge [draw=orange!70!black!90, color=orange!70!black!90, >=stealth, ->, line width=0.5mm,below, densely dashed] (tt);
\end{tikzpicture}
\end{center}
\end{frame}

\begin{frame}
\frametitle{Architecture of T3S Tool}
\begin{center}
\pgfdeclarelayer{background}
\pgfdeclarelayer{foreground}
\pgfsetlayers{background,main,foreground}
\begin{tikzpicture}[>=stealth', node distance=1cm, auto,]

\tikzstyle{punkt}=[rectangle,
	rounded corners,
	draw=black, very thick,
	text width=6.5em,
	minimum height=2em,
	text centered,
	drop shadow,
fill=white]

\tikzstyle{pil}=[->,
           thick,
           shorten <=2pt,
           shorten >=2pt]

\node[punkt] (model) {GSMP model};
\node[punkt, right=2.75cm of model] (se) {Sample executions};
\node[punkt, below=1.5cm of model, text width=5cm] (ms) {STA with estimated distributions};
\node[punkt, right=1.5cm of ms] (edpt) {Event driven prefix tree};
\node[punkt, below=1.5cm of edpt] (ise) {EDPT with changed clocks};
\node[punkt, below =1.5cm of ms, text width=5cm] (pss) {STA with equivalent states merged};

\node[below=0.6cm of pss] (dummy) {};
\node[right=0.5cm of dummy] (legend) {T3S algorithm};

\path (edpt) edge [->,left] node {SE} (ise)
(ise) edge [->,above] node {PSS} (pss)
(pss) edge [->,right] node {MS} (ms)
%(model) edge [->,above, bend left=35] node {} (edpt)
(ms) edge [->,left] node {Producing} (model)
(model) edge [->,above] node {Simulate} (se)
(se) edge [->,right] node {Creating} (edpt);

 \begin{pgfonlayer}{background}
	
	\path (ms)+(-3,1.0) node (g) {};
	\path (ise)+(1.8,-1.6) node (h) {};
	
	\path[fill=black!5,rounded corners, draw=black!50, dashed] (g) rectangle (h);
	
\end{pgfonlayer}
\end{tikzpicture}
\end{center}
\end{frame}

\begin{frame}
\frametitle{Sentences to known about the algorithm}
\begin{itemize}
\item Executions of stochastic processes, including GSMP, are typically \textbf{infinite}.
\item Thus, a \textbf{structurally complete set of sample executions} (SCS) with \textbf{finite} length is required (a burden for the user).
\begin{itemize}
\item The SCS have at least one passage in each \textbf{location} and each \textbf{event}.
\end{itemize}

\item Informally speaking the \textbf{difference} between the \textbf{reality} and the \textbf{model} tends to \textbf{zero} wrt. the amount of samples.
\begin{itemize}
\item The guarantees are given by the Kolmogorov-Smirnov test within $\alpha$ error. By the proof in \cite{csyu,jkzz}, we know that the $\beta$ error tends to infinite when sample execution size grows.
\end{itemize}

\end{itemize}
\end{frame}



\section{Evaluation of our approach - The T3S-Toolbox}

\begin{frame}{T3S-Tool}
\begin{itemize}
\item The tool is hosted on Google code in the following url: http://code.google.com/p/t3s-tool/

\item {How to compile:
\begin{itemize}
\item Get the last version from SVN with the following command:
{\tt svn checkout http://t3s-tool.googlecode.com/svn/trunk/ t3s-tool}
\item Install Matlab 7.11 (Windows or Linux)
\item Install the third party libraries: Qt 4.8.2, Graphicviz 2.28.0, and Qwt 6.0.1
\item Select the checkout folder in Matlab environment
\item Type {\tt Makefile} command (in Windows type {\tt Makefile\_Mingw32})\footnote{Note that you need Mingw tools for Windows.}
\end{itemize}
}
\end{itemize}
\end{frame}

\subsection{Empirical model}

\begin{frame}[fragile]
\frametitle{t3s\_demo}
\begin{figure}
\centering
\begin{itemize}
\item Please type 't3s\_demo' or 'framework\_example' (the last one for the older versions).
\end{itemize}
\begin{tikzpicture}
\node[scale=0.75]{
\begin{tikzpicture}[->, >=stealth', shorten >=1pt, auto, node distance=3cm, semithick]

\tikzstyle{every state}=[fill=white,draw=black,text=black]

\node[state]         (0) [minimum size=1.2cm] {$A$};
\node[state]         (1) [below of=0, minimum size=1.2cm] {$B$};
\node[state]         (2) [right of=1, minimum size=1.2cm] {$C$};

\path (0) edge [left] node {a} (1)
(0) edge [bend left, right] node {b} (2)
(1) edge [below] node {b} (2)
(2) edge [bend left, left] node {a} (0);

\end{tikzpicture}};
\end{tikzpicture}
\end{figure}
\vspace{-1.5cm}
\begin{verbatim}
module t3s_demo
state: [0..2];
[] (state=0) -> Wei(4.959164,1.046616) : (state'=2) +
  Wei(1.025079,1.015565) : (state'=1);
[] (state=1) -> Wei(4.959164,1.046616) : (state'=0);
[] (state=2) -> Wei(1.025079,1.015565) : (state'=1);
endmodule
\end{verbatim}

\end{frame}

\begin{frame}{t3s\_demo2 - One possible result}

\begin{figure}
\includegraphics[scale=0.35]{raster/t3s_demo2.png}
\end{figure}

\end{frame}


\begin{frame}{t3s\_demo2 - Another possible result}

\begin{figure}
\includegraphics[scale=0.25]{raster/t3s_demo2_1.png}
\end{figure}

\begin{itemize}
\item This depends essentially due to the learning parameters such as: number of execution samples, the length of the executions samples, and the significance of the samples.
\end{itemize}

\end{frame}


\begin{frame}[fragile]{t3s\_demo2}

\begin{verbatim}
module ts3_demo2
state: [0..4];
[] (state=0) -> Wei(4.479692,0.950557) : (state'=3) +
   Wei(0.906859,1.061059) : (state'=1) +
   Wei(1.943331,8.921822) : (state'=2);
[] (state=1) -> Wei(4.479692,0.950557) : (state'=0);
[] (state=2) -> Wei(0.906859,1.061059) : (state'=1) +
   Wei(1.943331,8.921822) : (state'=1);
[] (state=3) -> Wei(4.479692,0.950557) : (state'=1) +
   Wei(0.906859,1.061059) : (state'=4);
[] (state=4) -> Wei(1.943331,8.921822) : (state'=1) +
   Wei(0.906859,1.061059) : (state'=1);
endmodule
\end{verbatim}

\end{frame}


%\begin{frame}
%\frametitle{Two-processors scheduler model}
%
%\begin{minipage}{5.5cm}
%\begin{itemize}
%\item An 	\textbf{optimal scheduler design} for multi-processor systems with \textbf{uncertainty task duration} is a challenge
%\item With our method it is possible to \textbf{achieve answers} statistically:
%\begin{itemize}
%\item worst case sequence, and
%\item optimal case sequence.
%\end{itemize}
%\end{itemize}
%\end{minipage}
%\begin{minipage}{3cm}
%\begin{tikzpicture}\node[scale=0.5]{\begin{tikzpicture}[->, >=stealth', shorten >=1pt, auto, node distance=2.8cm, semithick]
%
%\tikzstyle{every state}=[fill=white,draw=black,text=black]
%
%\node[state,font=\scriptsize,fill=black!5]         (0) [minimum size=1.2cm] {$,,abc$};
%\node[state,font=\scriptsize]         (1) [minimum size=1.2cm, above right of=0] {$,ab,c$};
%\node[state,font=\scriptsize]         (2) [minimum size=1.2cm, right of=0] {$,ac,b$};
%\node[state,font=\scriptsize]         (3) [minimum size=1.2cm, below right of=0] {$,bc,a$};
%\node[state,font=\scriptsize]         (4) [minimum size=1.2cm, right of=1] {$A,bc,$};
%\node[state,font=\scriptsize]         (5) [minimum size=1.2cm, left of=0] {$B,ac,$};
%\node[state,font=\scriptsize]         (6) [minimum size=1.2cm, right of=3] {$C,ab,$};
%\node[state,font=\scriptsize]         (7) [minimum size=1.2cm, right of=4] {$AB,c,$};
%\node[state,font=\scriptsize]         (8) [minimum size=1.2cm, right of=6] {$BC,a,$};
%\node[state,font=\scriptsize]         (9) [node distance=2cm,minimum size=1.2cm, right of=2] {$AC,b,$};
%\node[state,font=\scriptsize,fill=black!5]         (10) [minimum size=1.2cm, right of=9] {$ABC,,$};
%
%\path (0) edge [below right] node {ab} (1)
%(0) edge [above right] node {ac} (2)
%(0) edge [] node {bc} (3)
%(1) edge [] node {a} (4)
%(1) edge [above] node {b} (5)
%(2) edge [] node {a} (4)
%(2) edge [] node {c} (6)
%(4) edge [] node {b} (7)
%(4) edge [] node {c} (9)
%(5) edge [bend left=40] node {a} (7)
%(5) edge [bend right=40,below] node {c} (8)
%(3) edge [] node {b} (5)
%(3) edge [] node {c} (6)
%(6) edge [] node {b} (8)
%(6) edge [] node {a} (9)
%(7) edge [] node {c} (10)
%(8) edge [] node {a} (10)
%(9) edge [] node {b} (10)
%;
%\end{tikzpicture}};
%\end{tikzpicture}
%\end{minipage}
%
%
%\end{frame}


\section{Conclusions and further work}

\begin{frame}
\frametitle{Conclusions and further work}

\begin{itemize}
\item Change definitions of equivalence relation (we can generalize statistically more or less given those definitions)
\item Our approach may be \textbf{scaled} for \textbf{larger systems},
\begin{itemize}
\item with an optimization of learning process.
\end{itemize}
\item Expand the proof of concept to other stochastic systems (not only for empirical models).
\end{itemize}

\end{frame}

\bibliographystyle{alpha}
\bibliography{lgsmp}

\end{document}
